\begin{tabbing}
$\forall$$i$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $x$:Id, $k$:Knd, $T$:Type, ${\it test}$:(State(${\it ds}$)$\rightarrow$$T$$\rightarrow\mathbb{B}$).
\\[0ex]$\neg$$x$ $\in$ dom(${\it ds}$)
\\[0ex]$\Rightarrow$ (isrcv($k$) $\Rightarrow$ $i$ $=$ destination(lnk($k$)))
\\[0ex]$\Rightarrow$ Normal($T$)
\\[0ex]$\Rightarrow$ Normal(${\it ds}$)
\\[0ex]$\Rightarrow$ \=R{-}base{-}recognize($i$;${\it ds}$;$x$;$k$;$T$;${\it test}$)\+
\\[0ex]$\Vdash$ ${\it es}$.\=vartype($i$;$x$) $\subseteq\rho$ $\mathbb{B}$ \& state@$i$ $\subseteq\rho$ State(${\it ds}$) \& kindtype($i$;$k$) $\subseteq\rho$ $T$\+
\\[0ex]\& \=$\forall$$e$@$i$.\+
\\[0ex]($x$ when $e$)
\\[0ex]$\Leftrightarrow$
\\[0ex]($\exists$${\it e'}$:E. (${\it e'}$ $<$loc $e$) \& kind(${\it e'}$) $=$ $k$ $\in$ Knd \& ${\it test}$((state when ${\it e'}$),val(${\it e'}$)))
\-\-\-
\end{tabbing}